(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).

Query: div(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

quotA(0, s(T208), T209, 0).
quotA(s(T226), s(T227), T228, T230) :- quotA(T226, T227, T228, T230).
quotA(T241, 0, T242, s(T244)) :- quotB(T241, s(T242), T244).
quotB(0, s(T15), 0).
quotB(s(0), s(s(T38)), 0).
quotB(s(s(0)), s(s(s(T61))), 0).
quotB(s(s(s(0))), s(s(s(s(T84)))), 0).
quotB(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0).
quotB(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0).
quotB(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0).
quotB(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0).
quotB(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) :- quotA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192).
quotB(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) :- quotC(T251, T253).
quotB(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) :- quotD(T350, T352).
quotB(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) :- quotE(T437, T439).
quotB(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) :- quotF(T512, T514).
quotB(s(s(s(T575))), s(s(s(0))), s(T577)) :- quotG(T575, T577).
quotB(s(s(T626)), s(s(0)), s(T628)) :- quotH(T626, T628).
quotB(s(T665), s(0), s(T667)) :- quotI(T665, T667).
quotC(0, 0).
quotC(s(0), 0).
quotC(s(s(0)), 0).
quotC(s(s(s(0))), 0).
quotC(s(s(s(s(0)))), 0).
quotC(s(s(s(s(s(0))))), 0).
quotC(s(s(s(s(s(s(0)))))), 0).
quotC(s(s(s(s(s(s(s(T336))))))), s(T338)) :- quotC(T336, T338).
quotD(0, 0).
quotD(s(0), 0).
quotD(s(s(0)), 0).
quotD(s(s(s(0))), 0).
quotD(s(s(s(s(0)))), 0).
quotD(s(s(s(s(s(0))))), 0).
quotD(s(s(s(s(s(s(T424)))))), s(T426)) :- quotD(T424, T426).
quotE(0, 0).
quotE(s(0), 0).
quotE(s(s(0)), 0).
quotE(s(s(s(0))), 0).
quotE(s(s(s(s(0)))), 0).
quotE(s(s(s(s(s(T500))))), s(T502)) :- quotE(T500, T502).
quotF(0, 0).
quotF(s(0), 0).
quotF(s(s(0)), 0).
quotF(s(s(s(0))), 0).
quotF(s(s(s(s(T564)))), s(T566)) :- quotF(T564, T566).
quotG(0, 0).
quotG(s(0), 0).
quotG(s(s(0)), 0).
quotG(s(s(s(T616))), s(T618)) :- quotG(T616, T618).
quotH(0, 0).
quotH(s(0), 0).
quotH(s(s(T656)), s(T658)) :- quotH(T656, T658).
quotI(0, 0).
quotI(s(T684), s(T686)) :- quotI(T684, T686).
divJ(T7, T8, T10) :- quotB(T7, T8, T10).

Query: divJ(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divJ_in: (b,b,f)
quotB_in: (b,b,f)
quotA_in: (b,b,b,f)
quotC_in: (b,f)
quotD_in: (b,f)
quotE_in: (b,f)
quotF_in: (b,f)
quotG_in: (b,f)
quotH_in: (b,f)
quotI_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quotC_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTC_IN_GA(T251, T253)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_GA(T336, T338, quotC_in_ga(T336, T338))
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_GGA(T350, T352, quotD_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTD_IN_GA(T350, T352)
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U12_GA(T424, T426, quotD_in_ga(T424, T426))
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_GGA(T437, T439, quotE_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTE_IN_GA(T437, T439)
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U13_GA(T500, T502, quotE_in_ga(T500, T502))
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_GGA(T512, T514, quotF_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTF_IN_GA(T512, T514)
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → U14_GA(T564, T566, quotF_in_ga(T564, T566))
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_GGA(T575, T577, quotG_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTG_IN_GA(T575, T577)
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → U15_GA(T616, T618, quotG_in_ga(T616, T618))
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U9_GGA(T626, T628, quotH_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTH_IN_GA(T626, T628)
QUOTH_IN_GA(s(s(T656)), s(T658)) → U16_GA(T656, T658, quotH_in_ga(T656, T658))
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U10_GGA(T665, T667, quotI_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTI_IN_GA(T665, T667)
QUOTI_IN_GA(s(T684), s(T686)) → U17_GA(T684, T686, quotI_in_ga(T684, T686))
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
DIVJ_IN_GGA(x1, x2, x3)  =  DIVJ_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
QUOTA_IN_GGGA(x1, x2, x3, x4)  =  QUOTA_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4)  =  U2_GGGA(x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x3)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quotC_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTC_IN_GA(T251, T253)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_GA(T336, T338, quotC_in_ga(T336, T338))
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_GGA(T350, T352, quotD_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTD_IN_GA(T350, T352)
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U12_GA(T424, T426, quotD_in_ga(T424, T426))
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_GGA(T437, T439, quotE_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTE_IN_GA(T437, T439)
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U13_GA(T500, T502, quotE_in_ga(T500, T502))
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_GGA(T512, T514, quotF_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTF_IN_GA(T512, T514)
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → U14_GA(T564, T566, quotF_in_ga(T564, T566))
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_GGA(T575, T577, quotG_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTG_IN_GA(T575, T577)
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → U15_GA(T616, T618, quotG_in_ga(T616, T618))
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U9_GGA(T626, T628, quotH_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTH_IN_GA(T626, T628)
QUOTH_IN_GA(s(s(T656)), s(T658)) → U16_GA(T656, T658, quotH_in_ga(T656, T658))
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U10_GGA(T665, T667, quotI_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTI_IN_GA(T665, T667)
QUOTI_IN_GA(s(T684), s(T686)) → U17_GA(T684, T686, quotI_in_ga(T684, T686))
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
DIVJ_IN_GGA(x1, x2, x3)  =  DIVJ_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
QUOTA_IN_GGGA(x1, x2, x3, x4)  =  QUOTA_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4)  =  U2_GGGA(x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x3)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 26 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTI_IN_GA(s(T684)) → QUOTI_IN_GA(T684)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTI_IN_GA(s(T684)) → QUOTI_IN_GA(T684)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GA(s(s(T656))) → QUOTH_IN_GA(T656)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTH_IN_GA(s(s(T656))) → QUOTH_IN_GA(T656)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(T616)))) → QUOTG_IN_GA(T616)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTG_IN_GA(s(s(s(T616)))) → QUOTG_IN_GA(T616)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(T564))))) → QUOTF_IN_GA(T564)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTF_IN_GA(s(s(s(s(T564))))) → QUOTF_IN_GA(T564)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T500)))))) → QUOTE_IN_GA(T500)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTE_IN_GA(s(s(s(s(s(T500)))))) → QUOTE_IN_GA(T500)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(s(s(T424))))))) → QUOTD_IN_GA(T424)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTD_IN_GA(s(s(s(s(s(s(T424))))))) → QUOTD_IN_GA(T424)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(52) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(53) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(54) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(s(s(s(s(T336)))))))) → QUOTC_IN_GA(T336)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(56) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTC_IN_GA(s(s(s(s(s(s(s(T336)))))))) → QUOTC_IN_GA(T336)
    The graph contains the following edges 1 > 1

(57) YES

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quotA_in_ggga(x1, x2, x3, x4)  =  quotA_in_ggga(x1, x2, x3)
quotA_out_ggga(x1, x2, x3, x4)  =  quotA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
QUOTA_IN_GGGA(x1, x2, x3, x4)  =  QUOTA_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(59) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(60) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)

R is empty.
The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
QUOTA_IN_GGGA(x1, x2, x3, x4)  =  QUOTA_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(61) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
QUOTA_IN_GGGA(s(T226), s(T227), T228) → QUOTA_IN_GGGA(T226, T227, T228)
QUOTA_IN_GGGA(T241, 0, T242) → QUOTB_IN_GGA(T241, s(T242))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(63) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTA_IN_GGGA(T241, 0, T242) → QUOTB_IN_GGA(T241, s(T242))
    The graph contains the following edges 1 >= 1

  • QUOTA_IN_GGGA(s(T226), s(T227), T228) → QUOTA_IN_GGGA(T226, T227, T228)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(64) YES